Nuprl Lemma : sum_unroll_unit_q
11,40
postcript
pdf
i
,
j
:
. (
i
+1 =
j
)
(
E
:({
i
..
j
}
).
i
k
<
j
.
E
(
k
) =
E
(
i
))
latex
Definitions
t
T
,
t
.1
,
CRng
,
<
+*>
,
|
r
|
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
Lemmas
crng
wf
,
qrng
wf
,
rng
sum
unroll
unit
origin
i, j:
. (i+1 = j) 
(E:({i..j
}
). 
i 
k < j. E(k) = E(i)) i, j:. (i+1 = j) (E:({i..j}). i k < j. E(k) = E(i)) 
T+*>x:A. B(x)a j < b. E(j)